$\forall$$k$:Knd, $T$, $B$:Type, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it tg}$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$$B$).
\\[0ex](isrcv($k$) $\Rightarrow$ destination(lnk($k$)) $=$ source($l$) $\in$ Id \& (lnk($k$) $=$ $l$ $\Rightarrow$ $T$ $=$ $B$ \& tag($k$) $=$ ${\it tg}$))
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal($B$)
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$)